T:Type, eq:EqDecider(T), es:ES, x, i:Id, v:T.
@i x initially v:T  e@i. ((x when e) = v)  (lastchange(x;e) < e) 

latex

Definitions	b, True, SQType(T), ff, tt, if b then t else f fi , {T}, @i(x:T), lastchange(x;e), P  Q, P  Q, P & Q, P  Q, , t  T, e@i. P(e), P  Q, EqDecider(T), x:A. B(x), ee'.P(e), (e <loc e'), A c B, @i x initially v:T, Unit, , False, Dec(P),
Lemmas	es-first-init, es-loc-init, es-init-le, es-init wf, es-vartype wf, es-isconst wf, not-changed, init-p-implies, last-change-property, Id sq, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, es-causl wf, es-causl irreflexivity, es-when wf, decidable es-causl, not wf, bnot wf, changed wf, assert wf, iff wf, bool wf, event system wf, init-p wf, es-E wf, es-loc wf, Id wf